Nuprl Lemma : l_member_set2
11,40
postcript
pdf
T
:Type,
P
:(
T
). (
x
:
T
. Dec(
P
(
x
)))
(
L
:({
x
:
T
|
P
(
x
)} List),
x
:
T
. (
x
L
)
(
x
L
))
latex
Definitions
t
T
,
f
(
a
)
,
x
(
s
)
,
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
.
t
(
x
)
,
Type
,
,
{
x
:
A
|
B
(
x
)}
,
type
List
,
x
:
A
B
(
x
)
,
S
T
,
{
T
}
,
Dec(
P
)
,
(
x
l
)
Lemmas
l
member
wf
,
decidable
wf
,
l
member
set
,
list-set-type-property
origin
T:Type, P:(T
). (x:T. Dec(P(x))) 
(L:({x:T| P(x)} List), x:T. (x 
L) (x L)) T:Type, P:(T). (x:T. Dec(P(x))) (L:({x:T| P(x)} List), x:T. (x L) (x L)) T
x.A(x)x:A. B(x) Q
x. t(x)B(x)
T l)